T:Type, P:(T), L1, L2:(T List).
no_repeats(T;L1)
 ((x:T. (x  L2)  ((x  L1) & ((P(x))))) & (x, y:T. x before y  L2  x before y  L1))
 (filter(P;L1) = L2) 

latex

Definitions	x:A  B(x), (x  l), b, P & Q, P  Q, x:AB(x), x:A. B(x), x before y  l, P  Q, , a < b, s = t, A, no_repeats(T;l), t  T, P  Q, Type, , type List, , f(a), Void, False
Lemmas	no repeats iff, iff wf, l member wf, assert wf, l before wf, no repeats wf, bool wf, filter-equals